Circuit designers and verification engineers use different methods to verify circuit designs. One common verification technique is simulation. Simulation dynamically verifies a design by monitoring behaviors of the design with respect to simulation test benches. Another verification technique is model checking. Model checking statically verifies properties of a design by analyzing the state space of the design and determining whether a property holds in all reachable states. The properties to verify may be global properties involving signals in widely separated parts of the design, or they may be more local properties that pertain only to single or small number of related modules in the design.
There are two distinct classes of local properties: built-in and user-specified. The built-in properties are those that can be inferred from the structure of the design, for example, the absence of arithmetic overflow, range overflow, index overflow, bus contention, multi-driven bus, divide by zero, and combinational cycles. The user-specified properties are those that are explicitly provided by the user, for example, as synthesis programs or as assertions defined in an assertion language.
Model checking has potential advantages over simulation. For example, no simulation test bench is required to run model checking. Moreover, model checking, unlike simulation, is exhaustive. On the other hand, model checking, due to computational limitations, generally cannot handle large designs.
Hence, designs should be partitioned into sufficiently small parts in order to model check a given property. Although presently capacity is not an issue for simulation of designs, it is foreseeable that in the future designs could be of a size that cannot be handled by a simulator as a whole. The partitioning may be used in design verification if the design variables in the partitions could be covered.
To determine if the variables are covered during design verification, a number of different traditional coverage metrics may be performed. However, the traditional methods cannot be used to determine coverage of variables in a design that is partitioned because they are not based on multiple categories of outcomes of property verifications. The traditional coverage metrics are only designed for simulation runs on the entire design, and not for verification of multiple partitions of a large design.